| Definitions | x:A  B(x),  x:A. B(x), glued(es; B; f; Ia; Ib), s = t, t  T, strong-subtype(A;B), P   Q, es-triggers(es;i;ds;conds), t.2, MaInterface(T), x:A  B(x), f(a), ES, Type, IdLnk, Id, ma-interface-consistent2(es;I), (x l), only events in L send on l with tg, glues(es; B; g; f; Ia; Ib),  b, a:A fp B(a), Atom$n, P & Q, x : v, f  g, e@i. P(e), a < b,  x:A. B(x), False, A c B,  A, k(v:B) sends on l [tg:T, f <state, v>]?[], let x,y = A in B(x;y), ma-interface-consistent-at(es;i;X), Inj(A;B;f), f is Q-R-pre-preserving on P, Q  = f== P, g glues Ia:Qa f Ib:Rb, valtype(e), rcv(l,tg), Knd,  , E, ma-interface-locs(I), ma-interface-dom(I;i), ma-interface-code(I;i;k),  x.A(x), ma-interface-valtype(I;i;k), es-in-port(es;l;tg), val(e), (state when e), KindDeq, f(x), outl(x), fpf-domain(f), t.1, x dom(f), hasloc(k;i), Top, left + right, State(ds), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi ,  x. t(x), P  Q, {x:A| B(x)} , Void,  , ma-interface-loc(I;i), [[I|i]],  , type List, S  T, sender(e), kind(e), source(l), ma-interface-conds(I;i), ma-interface-ds(I;i), ma-interface-consistent(es;X), IdDeq, P Q, <a, b>, ma-interface-info(I;i;k), f(x)?z, E(X), e  X, True,  T, Dec(P), b | a, a ~ b, a  b, a <p b, a < b, x f y, xL. P(x), (xL.P(x)), r s, r < s, q-rel(r;x), Outcome, l_disjoint(T;l1;l2), (e <loc e'), e loc e' , (e < e'), e c e', e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), es-r-immediate-pred(es;R;e';e), same-thread(es;p;e;e'), [e: i p j], [e: i p j], f2f+-pred(e',e), SqStable(P), a =!x:T. Q(x), InvFuns(A;B;f;g), IsEqFun(T;eq), Refl(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Trans(T;x,y.E(x;y)), AntiSym(T;x,y.R(x;y)), Connex(T;x,y.R(x;y)), CoPrime(a,b), Ident(T;op;id), Assoc(T;op), Comm(T;op), Inverse(T;op;id;inv), BiLinear(T;pl;tm), IsBilinear(A;B;C;+a;+b;+c;f), IsAction(A;x;e;S;f), Dist1op2opLR(A;1op;2op), fun_thru_1op(A;B;opa;opb;f), FunThru2op(A;B;opa;opb;f), Cancel(T;S;op), monot(T;x,y.R(x;y);f), IsMonoid(T;op;id), IsGroup(T;op;id;inv), IsMonHom{M1,M2}(f), a b, IsIntegDom(r), IsPrimeIdeal(R;P), f g, X(e), Unit, ff, inr x , locl(a), tt, inl x , EqDecider(T), EOrderAxioms(E; pred?; info), EState(T), x,y. t(x;y), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M),  ,  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', constant_function(f;A;B), loc(e), kind(e), acttype(e), rcvtype(e),  x:A.B(x), vartype(i;x), {T}, es-first-from(es;e;l;tg), isrcv(k), isrcv(e), state@i, s ~ t, do-apply(f;x), p q, a = b, loc(e), SQType(T), P  Q, AbsInterface(A) |
| Lemmas | ma-interface-subtype, assert-eq-knd, ma-interface-triggers-kind, decidable equal Kind, decidable l member, ma-interface-triggers-loc, assert-eq-id, not functionality wrt iff, assert of bnot, iff transitivity, or functionality wrt iff, assert of bor, bnot thru band, eqff to assert, and functionality wrt iff, assert of band, eqtt to assert, ma-interface-triggers-do-apply, es-val wf, es-state-when wf, pi2 wf, outl wf, es-kind-rcv, es-is-interface-in-port, es-isrcv wf, es-sender wf, es-in-port wf, es-interface-val wf, es-rcvtype wf, es-acttype wf, constant function wf, qle wf, cless wf, val-axiom wf, rationals wf, nat wf, Msg wf, kindcase wf, EState wf, EOrderAxioms wf, deq wf, locl wf, btrue wf, bfalse wf, unit wf, bool wf, glues wf, es-E-interface wf, sq stable from decidable, decidable assert, es-is-interface wf, subtype-set-hasloc, subtype rel set, subtype rel function, subtype rel list, subtype rel product, l member subtype, ma-interface-triggers wf, glued wf, ma-interface-code wf, ma-interface-valtype wf, ma-interface-dom wf, hasloc wf, l member wf, lsrc wf, ma-interface-locs wf, es-E wf, es-kind wf, rcv wf, es-valtype wf, ma-interface-consistent2 wf, IdLnk wf, ma-interface wf, event system wf, ma-interface-consistent-consistent2, sender-frame-glues-triggers, fpf-dom wf, Kind-deq wf, ma-interface-conds wf3, Id wf, ifthenelse wf, ma-interface-conds wf2, member wf, subtype rel wf, fpf-trivial-subtype-top, fpf wf, assert wf, sframe-p wf, member-fpf-domain, ma-interface-dom-hasloc, ma-interface-conds wf, Knd wf, fpf-ap wf, top wf, decl-state wf, pi1 wf, conditional-send-p wf, ma-interface-ds wf |
